import java.util.HashMap;

import apron.Abstract1;
import apron.ApronException;
import apron.Box;
import apron.Environment;
import apron.Interval;
import apron.Linexpr1;
import apron.Manager;
import apron.MpqScalar;

public class Utils {

	public static Interval newTop() {
		Interval top = new Interval();
		top.setTop();
		return top;
	}

	/**
	 * Creates a new bottom interval, forces the interval to be of type integer
	 * (Mpq) and not floating point (Mpfr).
	 */
	public static Interval newBottom() {
		Interval bottom = new Interval();
		bottom.setInf(new MpqScalar(1));
		bottom.setSup(new MpqScalar(-1));
		return bottom;
	}

	public static Interval[] createBottomIntervals(String[] vars) {
		Interval[] result = new Interval[vars.length];

		for (int i = 0; i < vars.length; i++) {
			result[i] = newBottom();
		}

		return result;
	}

	public static Interval[] createTopIntervals(String[] vars) {
		Interval[] result = new Interval[vars.length];

		for (int i = 0; i < vars.length; i++) {
			result[i] = newTop();
		}

		return result;
	}

	public static Interval JoinIntervals(Interval src1Interval,
			Interval src2Interval) {
		String[] bnames = { "tmpVar" };
		Environment env = new Environment(bnames, new String[0]);
		Box b1 = new Box();
		try {
			Abstract1 xa0 = new Abstract1(b1, env, bnames,
					new Interval[] { src1Interval });
			Abstract1 xa1 = new Abstract1(b1, env, bnames,
					new Interval[] { src2Interval });
			xa0.join(b1, xa1);
			return xa0.toBox(b1)[0];
		} catch (ApronException e) {
			e.printStackTrace();
			return null;
		}
	}

	public static Interval MeetIntervals(Interval src1Interval,
			Interval src2Interval) {
		String[] bnames = { "tmpVar" };
		Environment env = new Environment(bnames, new String[0]);
		Box b1 = new Box();
		try {
			Abstract1 xa0 = new Abstract1(b1, env, bnames,
					new Interval[] { src1Interval });
			Abstract1 xa1 = new Abstract1(b1, env, bnames,
					new Interval[] { src2Interval });
			xa0.meet(b1, xa1);
			return xa0.toBox(b1)[0];
		} catch (ApronException e) {
			e.printStackTrace();
			return null;
		}
	}

	public static Interval WidenIntervals(Interval src1Interval,
			Interval src2Interval) {
		String[] bnames = { "tmpVar" };
		Environment env = new Environment(bnames, new String[0]);
		Box b1 = new Box();
		try {
			Abstract1 xa0 = new Abstract1(b1, env, bnames,
					new Interval[] { src1Interval });
			Abstract1 xa1 = new Abstract1(b1, env, bnames,
					new Interval[] { src2Interval });
			xa0 = xa1.isBottom(b1) ? xa0 : xa0.widening(b1, xa1);
			return xa0.toBox(b1)[0];
		} catch (ApronException e) {
			e.printStackTrace();
			return null;
		}
	}

	public static HashMap<String, Interval> getVaribaleValues(
			Abstract1 currState, HashMap<String, Boolean> bottomMap, Manager m) {

		HashMap<String, Interval> result = new HashMap<String, Interval>();

		try {
			String[] varNames = currState.getEnvironment().getIntVars();
			Interval[] boxValues = currState.toBox(m);
			for (int i = 0; i < varNames.length; i++) {

				if (bottomMap.get(varNames[i])) {
					result.put(varNames[i], Utils.newBottom());
				} else {
					result.put(varNames[i], boxValues[i]);
				}
			}

		} catch (ApronException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}

		return result;

	}

	public static HashMap<String, Interval> getExpressionRelevantValues(
			HashMap<String, Interval> varValues, Linexpr1 l) {
		HashMap<String, Interval> result = new HashMap<String, Interval>();

		String[] relevantVars = l.getEnvironment().getVars();

		for (String s : relevantVars) {
			result.put(s, varValues.get(s));
		}
		return result;
	}

	public static Interval[] getValuesOf(String[] variables,
			HashMap<String, Interval> state) {
		Interval[] result = new Interval[variables.length];
		for (int i = 0; i < variables.length; i++) {
			if (state.containsKey(variables[i])) {
				result[i] = state.get(variables[i]);
			} else {
				result[i] = newTop();
			}
		}
		return result;
	}
}
